package alloy.bool;

import java.io.File;
import java.io.IOException;

import alloy.util.Flag;
import alloy.util.ProcessInfo;

/**
 * Process wrapper class for running SAT-related processes, specifically
 * sat2cnf and the SAT solvers.  These processes use a predefined
 * protocol for how to tell the process to terminate, how to
 * interpret the outcome of the process, etc.  This class provides
 * convenience methods that take advantage of this protocol.
 * On the C++ side, programs adhere to the protocol by calling
 * methods of SatLab/src/solvctrl/SC_SolverControl.
 * <p>
 * The protocol, in brief:
 *   -- to tell a program to terminate: write a "0" (zero) to its stdin
 *   -- when the program is done, it prints a predefined string,
 *      defined as {@link BLBackend#OUTCOME_PREFIX}, followed by
 *      one of the outcome values: {@link BLBackend#NORMAL_TERMINATION},
 *      {@link BLBackend#CANCELLED_BY_USER}, {@link BLBackend#ENVIRONMENTAL_ERROR},
 *      {@link BLBackend#INTERNAL_ERROR}, optionally followed by an explanatory
 *      text string (for error outcomes).
 */
class SATProcessInfo extends ProcessInfo {
    /** Prefix that identifies the outcome in the output. */
    static final String OUTCOME_PREFIX = "======> Outcome: ";

    /** Outcome indicating normal termination. */
    public static final int NORMAL_TERMINATION = 0;
    
    /**
     * Outcome indicating that the SAT program was cancelled
     * by the user (by calling {@link BLBackend#interruptSolver}).
     */
    
    public static final int CANCELLED_BY_USER = 1;
    
    /**
     * Outcome indicating a correctable environmental error,
     * such as out-of-memory or out-of-disc-space.
     */
    public static final int ENVIRONMENTAL_ERROR = 2;
    
    /** Outcome indicating an internal error in the SAT program. */
    public static final int INTERNAL_ERROR = 3;

    /**
     * Outcome of this run of the SAT program -- set when
     * {@link #runUntilOutcome} returns.
     */
    private int _outcome;

    /**
     * Message accompanying the outcome -- set when
     * {@link #runUntilOutcome} returns.
     */
    private String _outcomeMsg;
    
    /** Start the given SAT process; die if there is any error. */
    SATProcessInfo(String processName_, String[] processArgs_, File dir) throws IOException {
	super(processName_, processArgs_, dir);
    }

    /**
     * Run the SAT process until it prints an outcome line,
     * or until it crashes.  Return the outcome value;
     * outcome string may be retrieved later by calling
     * {@link #getOutcomeMsg}.
     * <p>
     * Note that this will never return unless the running
     * process either terminates or crashes.  (Of course
     * the user can terminate the process prematurely
     * by giving an abort command.)
     */
    int runUntilOutcome(Runnable readStartedCallback_) {
      final StringBuffer lastLineBuf = new StringBuffer();
      final Flag lastLineSet = new Flag(false);
      ProcessInfo.ProcessOutputListener
	  outcomeLineListener =
	  new ProcessInfo.ProcessOutputListener() {
	      public boolean processLine(String line_) {
		  // terminate iff a specially marked line is detected
		  // in sat2cnf's output
		  if (line_.startsWith(OUTCOME_PREFIX)) {
		      lastLineBuf.append(line_);
		      lastLineSet.setValue(true);
		      if (alloy.util.FileUtil.runningOnWindows()  &&
			  _extractOutcome(line_) == NORMAL_TERMINATION) {
			  sendLine("0");
		      }
		      return false;  // do not continue
		  } else return true;  // continue
	      }};
      if (readStartedCallback_ == null)
	  runProcess(outcomeLineListener);
      else
	  runProcess(outcomeLineListener, readStartedCallback_);

      if (!lastLineSet.getValue())
	  // terminated without printing the specially marked line --
	  // so it must have crashed.
	  lastLineBuf.append(OUTCOME_PREFIX + INTERNAL_ERROR + " Unexpected termination");
      String lastLine = lastLineBuf.toString();
	
      _outcome = _extractOutcome(lastLine);
      _outcomeMsg = _extractOutcomeMsg(lastLine);
      
      return _outcome;
    }  // runUntilOutcome()

    /**
     * Run the SAT process until it prints an outcome line,
     * or until it crashes.  Return the outcome value;
     * outcome string may be retrieved later by calling
     * {@link #getOutcomeMsg}.
     * <p>
     * Note that this will never return unless the running
     * process either terminates or crashes.  (Of course
     * the user can terminate the process prematurely
     * by giving an abort command.)
     */
    int runUntilOutcome() { return runUntilOutcome(null); }

    /** @return the outcome, after {@link #runUntilOutcome} returns */
    int getOutcome() { return _outcome; }

    /** @return the outcome message, after {@link #runUntilOutcome} returns */
    String getOutcomeMsg() { return _outcomeMsg; }
    

    /** Extract the outcome value from the outcome string. */
    private int _extractOutcome(String line_) {
	StringBuffer outcomeNum = new StringBuffer();
	for (int i=OUTCOME_PREFIX.length(); i<line_.length(); i++) {
	    char c = line_.charAt(i);
	    if (Character.isDigit(c))
		outcomeNum.append(c);
	    else
		break;
	}
	try { return Integer.valueOf(outcomeNum.toString()).intValue(); }
	catch (NumberFormatException nfe_) { return INTERNAL_ERROR; }
    }

    /** Extract the message from the outcome string. */
    private String _extractOutcomeMsg(String line_) {
	StringBuffer outcomeNum = new StringBuffer();
	int i=OUTCOME_PREFIX.length();
	for (; i<line_.length(); i++) {
	    char c = line_.charAt(i);
	    if (Character.isDigit(c))
		outcomeNum.append(c);
	    else
		break;
	}
	return line_.substring(i);
    }
}  // class SATProcessInfo
